when-after(e;info;pred?;init;Trans;val)
== if first(e) <x.init(loc(e),x),Trans(loc(e),kind(e),val(e),x.init(loc(e),x))>
== else let p = when-after(pred(e);info;pred?;init;Trans;val) in 
== else <2of(p),Trans(loc(e),kind(e),val(e),2of(p))> fi
(recursive) 

latex

---

clarification:

when-after(e;info;pred?;init;Trans;val)
== if first(pred?;e)
== if <x.init(loc(info;e),x),Trans(loc(info;e),kind(info;e),val(e),x.init(loc(info;e),x))>
== else let p = when-after(pred(pred?;e);info;pred?;init;Trans;val) in 
== else <2of(p),Trans(loc(info;e),kind(info;e),val(e),2of(p))> fi
(recursive) 

latex

Definitions	Y, if b t else f fi, first(e), x.A(x), let x = a in b(x), pred(e), <a,b>, loc(e), kind(e), f(a), 2of(t)
FDL editor aliases	when-after